\begin{tabbing}
state{-}machine{-}spec\=\{i:l\}\+
\\[0ex](${\it es}$; $C$; $R$; $F$; $I$; $O$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$\=$X$:AbsInterface($C$)\+
\\[0ex]$\exists$\=$Q$:E$\rightarrow$E$\rightarrow\mathbb{P}$\+
\\[0ex]$\exists$\=$B$:retrace(${\it es}$; $Q$; $X$)\+
\\[0ex](Q{-}R{-}glued(${\it es}$; $C$; ($\lambda$$e$.$I$($e$)); $I$; ($\lambda$$e$,${\it e'}$. ($e$ $<$loc ${\it e'}$)); $X$; $Q$)
\\[0ex]\& Q{-}R{-}glued(\=${\it es}$;\+
\\[0ex]$R$;
\\[0ex]($\lambda$$e$.$F$(map($\lambda$${\it e'}$.$X$(${\it e'}$);(retracer($B$)($e$)) @ [$e$])));
\\[0ex]$X$;
\\[0ex]$Q$;
\\[0ex]$O$;
\\[0ex]($\lambda$$e$,${\it e'}$. (loc($e$) = loc(${\it e'}$)) $\Rightarrow$ ($e$ $<$loc ${\it e'}$))))
\-\-\-\-
\end{tabbing}